/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.anno;

import static com.googlecode.syper.anno.Pred.ensures;
import static com.googlecode.syper.anno.Pred.forall;

import java.lang.annotation.ElementType;
import java.lang.annotation.Target;

import com.googlecode.syper.anno.Pred.IntPred;

/**
 * Marks a local variable as holding the pre-image of a field or
 * of the contents of an array.
 * Locals annotated with this annotation must be initialized in the declaration
 * and should be declared {@code final} (to prevent accidental modification).
 * Locals holding the contents of an array should also be annotated with
 * {@link Imm} to prevent modification of the array's contents.
 * The pre-image is the value of the field as it was when a method was entered.
 * This is similar to JMS's {@code \old} and Spec#'s {@code old}.
 *
 * Initialize <b>before doing anything else in a method</b>:
 * <ul>
 * <li>old field values with a field of the receiver or a local variable
 * <li>old array contents (first dimension) with a call to
 * {@link Arrays#copyOf} that copies the array
 * <li>contents of the second or greater dimension of an array with a call to
 * {@link Arrays#copyOf(Object[], int)} that copies the array up to the desired
 * depth
 * </ul>
 * Note that the old old contents of an array are different from
 * the old contents of the second dimension of that array.
 * They have to be kept in separate locals annotated with {@link Old}
 * @author kevin
 */
@Target({ ElementType.LOCAL_VARIABLE })
public @interface Old {
	/**
	 * Do not provide this attribute for old field values (or use 0)
	 * and indicate the array dimension copied for old contents of an array.
	 * Typically this value will be 1, indicating the old content of a
	 * 1-dimensional array.
	 * If the copied array has multiple dimensions this attribute should be 1
	 * to refer to the pre-image of the first dimension of the array, 2 to refer
	 * to the pre-image of the second dimension, and so on.
	 */
	public int dim() default 0;

	/**
	 * Use the methods in this class to initialize local variables annotated
	 * as {@link Old} with a copy of an array.
	 * @author kevin
	 * @since Dec 29, 2010
	 * @see java.util.Arrays
	 */
	public static class Arrays {

		/** static members only */
		private Arrays() {}

		/**
		 * Copies the elements of an array of objects (including arrays
		 * of arrays) into a new array of equal length.
		 * To make deep copies of multi-dimensional arrays use
		 * {@link #copyOf(Object[], int)}.
		 * @param <T> array element type
		 * @param a the array to copy or {@code null}
		 * @return new array of equal length with {@code a}'s elements
		 * or {@code null} if {@code a} is {@code null}
		 */
		@ReturnExcl public static <T> T[] copyOf(@Imm final T[] a) {
			@Result final T[] result =
				a == null ? null : java.util.Arrays.copyOf(a, a.length);
			ensures(a == null ? result == null :
				result != null & result != a & result.length == a.length
				& forall(0, result.length, new IntPred() {
					public boolean cond(int k) { return result[k] == a[k]; }
				}));
			return result;
		}

		/**
		 * Makes a deep copy of a multi-dimensional array up to the specified
		 * {@code depth}.
		 * If {@code depth} is 1 then the effect of this method is the same
		 * as {@link #copyOf(Object[])}.
		 * @param <T> array type with at least {@code depth - 1} dimensions
		 * @param a array with at least {@code depth} dimensions or {@code null}
		 * @param depth number of dimensions to copy
		 * @return a deep copy of a multi-dimensional array up to the specified
		 * {@code depth} or {@code null} if {@code a} was {@code null}.
		 */
		@SuppressWarnings("unchecked")
		@ReturnExcl public static <T> T[] copyOf(@Imm T[] a, int depth) {
			if (depth <= 0)
				throw new IllegalArgumentException("not positive: " + depth);
			final T[] result = copyOf(a);
			if (a == null || depth == 1 || a.length == 0)
				return result;
			for (int i = 0; i < result.length; ++i) {
				Class<?> elemClass = result[i].getClass();
				if (byte[].class == elemClass)
					result[i] = (T) elemClass.cast(copyOf((byte[]) result[i]));
				else if (short[].class == elemClass)
					result[i] = (T) elemClass.cast(copyOf((short[]) result[i]));
				else if (int[].class == elemClass)
					result[i] = (T) elemClass.cast(copyOf((int[]) result[i]));
				else if (long[].class == elemClass)
					result[i] = (T) elemClass.cast(copyOf((long[]) result[i]));
				else if (char[].class == elemClass)
					result[i] = (T) elemClass.cast(copyOf((char[]) result[i]));
				else if (float[].class == elemClass)
					result[i] = (T) elemClass.cast(copyOf((float[]) result[i]));
				else if (double[].class == elemClass)
					result[i] = (T) elemClass.cast(copyOf((double[]) result[i]));
				else if (boolean[].class == elemClass)
					result[i] = (T) elemClass.cast(copyOf((boolean[]) result[i]));
				else if (elemClass.isArray()) {
					// this case includes arrays of primitive arrays
					result[i] = (T) elemClass.cast(copyOf((Object[]) result[i], depth - 1));
					// skip depth check below
					continue;
				} else
					throw new IllegalArgumentException("Not enough dimensions");
				if (2 < depth)
					throw new IllegalArgumentException("Not enough dimensions");
			}
			return result;
		}

		/**
		 * Copies the elements of a {@code byte} array
		 * into a new array of equal length.
		 * To make deep copies of multi-dimensional arrays use
		 * {@link #copyOf(Object[], int)}.
		 * @param a the array to copy or {@code null}
		 * @return new array of equal length with {@code a}'s elements
		 * or {@code null} if {@code a} is {@code null}
		 */
		@ReturnExcl public static byte[] copyOf(@Imm final byte[] a) {
			@Result final byte[] result =
				a == null ? null : java.util.Arrays.copyOf(a, a.length);
			ensures(a == null ? result == null :
				result != null & result != a & result.length == a.length
				& forall(0, result.length, new IntPred() {
					public boolean cond(int k) { return result[k] == a[k]; }
				}));
			return result;
		}

		/**
		 * Copies the elements of a {@code short} array
		 * into a new array of equal length.
		 * To make deep copies of multi-dimensional arrays use
		 * {@link #copyOf(Object[], int)}.
		 * @param a the array to copy or {@code null}
		 * @return new array of equal length with {@code a}'s elements
		 * or {@code null} if {@code a} is {@code null}
		 */
		@ReturnExcl public static short[] copyOf(@Imm final short[] a) {
			@Result final short[] result =
				a == null ? null : java.util.Arrays.copyOf(a, a.length);
			ensures(a == null ? result == null :
				result != null & result != a & result.length == a.length
				& forall(0, result.length, new IntPred() {
					public boolean cond(int k) { return result[k] == a[k]; }
				}));
			return result;
		}

		/**
		 * Copies the elements of a {@code int} array
		 * into a new array of equal length.
		 * To make deep copies of multi-dimensional arrays use
		 * {@link #copyOf(Object[], int)}.
		 * @param a the array to copy or {@code null}
		 * @return new array of equal length with {@code a}'s elements
		 * or {@code null} if {@code a} is {@code null}
		 */
		@ReturnExcl public static int[] copyOf(@Imm final int[] a) {
			@Result final int[] result =
				a == null ? null : java.util.Arrays.copyOf(a, a.length);
			ensures(a == null ? result == null :
				result != null & result != a & result.length == a.length
				& forall(0, result.length, new IntPred() {
					public boolean cond(int k) { return result[k] == a[k]; }
				}));
			return result;
		}

		/**
		 * Copies the elements of a {@code long} array
		 * into a new array of equal length.
		 * To make deep copies of multi-dimensional arrays use
		 * {@link #copyOf(Object[], int)}.
		 * @param a the array to copy or {@code null}
		 * @return new array of equal length with {@code a}'s elements
		 * or {@code null} if {@code a} is {@code null}
		 */
		@ReturnExcl public static long[] copyOf(@Imm final long[] a) {
			@Result final long[] result =
				a == null ? null : java.util.Arrays.copyOf(a, a.length);
			ensures(a == null ? result == null :
				result != null & result != a & result.length == a.length
				& forall(0, result.length, new IntPred() {
					public boolean cond(int k) { return result[k] == a[k]; }
				}));
			return result;
		}

		/**
		 * Copies the elements of a {@code char} array
		 * into a new array of equal length.
		 * To make deep copies of multi-dimensional arrays use
		 * {@link #copyOf(Object[], int)}.
		 * @param a the array to copy or {@code null}
		 * @return new array of equal length with {@code a}'s elements
		 * or {@code null} if {@code a} is {@code null}
		 */
		@ReturnExcl public static char[] copyOf(@Imm final char[] a) {
			@Result final char[] result =
				a == null ? null : java.util.Arrays.copyOf(a, a.length);
			ensures(a == null ? result == null :
				result != null & result != a & result.length == a.length
				& forall(0, result.length, new IntPred() {
					public boolean cond(int k) { return result[k] == a[k]; }
				}));
			return result;
		}

		/**
		 * Copies the elements of a {@code float} array
		 * into a new array of equal length.
		 * To make deep copies of multi-dimensional arrays use
		 * {@link #copyOf(Object[], int)}.
		 * @param a the array to copy or {@code null}
		 * @return new array of equal length with {@code a}'s elements
		 * or {@code null} if {@code a} is {@code null}
		 */
		@ReturnExcl public static float[] copyOf(@Imm final float[] a) {
			@Result final float[] result =
				a == null ? null : java.util.Arrays.copyOf(a, a.length);
			ensures(a == null ? result == null :
				result != null & result != a & result.length == a.length
				& forall(0, result.length, new IntPred() {
					public boolean cond(int k) { return result[k] == a[k]; }
				}));
			return result;
		}

		/**
		 * Copies the elements of a {@code double} array
		 * into a new array of equal length.
		 * To make deep copies of multi-dimensional arrays use
		 * {@link #copyOf(Object[], int)}.
		 * @param a the array to copy or {@code null}
		 * @return new array of equal length with {@code a}'s elements
		 * or {@code null} if {@code a} is {@code null}
		 */
		@ReturnExcl public static double[] copyOf(@Imm final double[] a) {
			@Result final double[] result =
				a == null ? null : java.util.Arrays.copyOf(a, a.length);
			ensures(a == null ? result == null :
				result != null & result != a & result.length == a.length
				& forall(0, result.length, new IntPred() {
					public boolean cond(int k) { return result[k] == a[k]; }
				}));
			return result;
		}

		/**
		 * Copies the elements of a {@code boolean} array
		 * into a new array of equal length.
		 * To make deep copies of multi-dimensional arrays use
		 * {@link #copyOf(Object[], int)}.
		 * @param a the array to copy or {@code null}
		 * @return new array of equal length with {@code a}'s elements
		 * or {@code null} if {@code a} is {@code null}
		 */
		@ReturnExcl public static boolean[] copyOf(@Imm final boolean[] a) {
			@Result final boolean[] result =
				a == null ? null : java.util.Arrays.copyOf(a, a.length);
			ensures(a == null ? result == null :
				result != null & result != a & result.length == a.length
				& forall(0, result.length, new IntPred() {
					public boolean cond(int k) { return result[k] == a[k]; }
				}));
			return result;
		}
	}
}
